Termination w.r.t. Q proof of TRS/TRCSREx9_Luc04

Termination w.r.t. Q of the following Term Rewriting System could not be shown:

Q restricted rewrite system:
The TRS R consists of the following rules:

active(f(a, b, X)) → mark(f(X, X, X))
active(c) → mark(a)
active(c) → mark(b)
active(f(X1, X2, X3)) → f(active(X1), X2, X3)
active(f(X1, X2, X3)) → f(X1, X2, active(X3))
f(mark(X1), X2, X3) → mark(f(X1, X2, X3))
f(X1, X2, mark(X3)) → mark(f(X1, X2, X3))
proper(f(X1, X2, X3)) → f(proper(X1), proper(X2), proper(X3))
proper(a) → ok(a)
proper(b) → ok(b)
proper(c) → ok(c)
f(ok(X1), ok(X2), ok(X3)) → ok(f(X1, X2, X3))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))

Q is empty.

↳ QTRS

Q restricted rewrite system:
The TRS R consists of the following rules:

active(f(a, b, X)) → mark(f(X, X, X))
active(c) → mark(a)
active(c) → mark(b)
active(f(X1, X2, X3)) → f(active(X1), X2, X3)
active(f(X1, X2, X3)) → f(X1, X2, active(X3))
f(mark(X1), X2, X3) → mark(f(X1, X2, X3))
f(X1, X2, mark(X3)) → mark(f(X1, X2, X3))
proper(f(X1, X2, X3)) → f(proper(X1), proper(X2), proper(X3))
proper(a) → ok(a)
proper(b) → ok(b)
proper(c) → ok(c)
f(ok(X1), ok(X2), ok(X3)) → ok(f(X1, X2, X3))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))

Q is empty.